tower1(x) -> f3(a, x, s1(0))
f3(a, 0, y) -> y
f3(a, s1(x), y) -> f3(b, y, s1(x))
f3(b, y, x) -> f3(a, half1(x), exp1(y))
exp1(0) -> s1(0)
exp1(s1(x)) -> double1(exp1(x))
double1(0) -> 0
double1(s1(x)) -> s1(s1(double1(x)))
half1(0) -> double1(0)
half1(s1(0)) -> half1(0)
half1(s1(s1(x))) -> s1(half1(x))
↳ QTRS
↳ DependencyPairsProof
tower1(x) -> f3(a, x, s1(0))
f3(a, 0, y) -> y
f3(a, s1(x), y) -> f3(b, y, s1(x))
f3(b, y, x) -> f3(a, half1(x), exp1(y))
exp1(0) -> s1(0)
exp1(s1(x)) -> double1(exp1(x))
double1(0) -> 0
double1(s1(x)) -> s1(s1(double1(x)))
half1(0) -> double1(0)
half1(s1(0)) -> half1(0)
half1(s1(s1(x))) -> s1(half1(x))
DOUBLE1(s1(x)) -> DOUBLE1(x)
EXP1(s1(x)) -> DOUBLE1(exp1(x))
HALF1(0) -> DOUBLE1(0)
EXP1(s1(x)) -> EXP1(x)
F3(b, y, x) -> EXP1(y)
TOWER1(x) -> F3(a, x, s1(0))
F3(b, y, x) -> F3(a, half1(x), exp1(y))
HALF1(s1(s1(x))) -> HALF1(x)
HALF1(s1(0)) -> HALF1(0)
F3(b, y, x) -> HALF1(x)
F3(a, s1(x), y) -> F3(b, y, s1(x))
tower1(x) -> f3(a, x, s1(0))
f3(a, 0, y) -> y
f3(a, s1(x), y) -> f3(b, y, s1(x))
f3(b, y, x) -> f3(a, half1(x), exp1(y))
exp1(0) -> s1(0)
exp1(s1(x)) -> double1(exp1(x))
double1(0) -> 0
double1(s1(x)) -> s1(s1(double1(x)))
half1(0) -> double1(0)
half1(s1(0)) -> half1(0)
half1(s1(s1(x))) -> s1(half1(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
DOUBLE1(s1(x)) -> DOUBLE1(x)
EXP1(s1(x)) -> DOUBLE1(exp1(x))
HALF1(0) -> DOUBLE1(0)
EXP1(s1(x)) -> EXP1(x)
F3(b, y, x) -> EXP1(y)
TOWER1(x) -> F3(a, x, s1(0))
F3(b, y, x) -> F3(a, half1(x), exp1(y))
HALF1(s1(s1(x))) -> HALF1(x)
HALF1(s1(0)) -> HALF1(0)
F3(b, y, x) -> HALF1(x)
F3(a, s1(x), y) -> F3(b, y, s1(x))
tower1(x) -> f3(a, x, s1(0))
f3(a, 0, y) -> y
f3(a, s1(x), y) -> f3(b, y, s1(x))
f3(b, y, x) -> f3(a, half1(x), exp1(y))
exp1(0) -> s1(0)
exp1(s1(x)) -> double1(exp1(x))
double1(0) -> 0
double1(s1(x)) -> s1(s1(double1(x)))
half1(0) -> double1(0)
half1(s1(0)) -> half1(0)
half1(s1(s1(x))) -> s1(half1(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
DOUBLE1(s1(x)) -> DOUBLE1(x)
tower1(x) -> f3(a, x, s1(0))
f3(a, 0, y) -> y
f3(a, s1(x), y) -> f3(b, y, s1(x))
f3(b, y, x) -> f3(a, half1(x), exp1(y))
exp1(0) -> s1(0)
exp1(s1(x)) -> double1(exp1(x))
double1(0) -> 0
double1(s1(x)) -> s1(s1(double1(x)))
half1(0) -> double1(0)
half1(s1(0)) -> half1(0)
half1(s1(s1(x))) -> s1(half1(x))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DOUBLE1(s1(x)) -> DOUBLE1(x)
POL( DOUBLE1(x1) ) = max{0, x1 - 2}
POL( s1(x1) ) = x1 + 3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
tower1(x) -> f3(a, x, s1(0))
f3(a, 0, y) -> y
f3(a, s1(x), y) -> f3(b, y, s1(x))
f3(b, y, x) -> f3(a, half1(x), exp1(y))
exp1(0) -> s1(0)
exp1(s1(x)) -> double1(exp1(x))
double1(0) -> 0
double1(s1(x)) -> s1(s1(double1(x)))
half1(0) -> double1(0)
half1(s1(0)) -> half1(0)
half1(s1(s1(x))) -> s1(half1(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
HALF1(s1(s1(x))) -> HALF1(x)
tower1(x) -> f3(a, x, s1(0))
f3(a, 0, y) -> y
f3(a, s1(x), y) -> f3(b, y, s1(x))
f3(b, y, x) -> f3(a, half1(x), exp1(y))
exp1(0) -> s1(0)
exp1(s1(x)) -> double1(exp1(x))
double1(0) -> 0
double1(s1(x)) -> s1(s1(double1(x)))
half1(0) -> double1(0)
half1(s1(0)) -> half1(0)
half1(s1(s1(x))) -> s1(half1(x))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
HALF1(s1(s1(x))) -> HALF1(x)
POL( HALF1(x1) ) = max{0, x1 - 3}
POL( s1(x1) ) = x1 + 2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
tower1(x) -> f3(a, x, s1(0))
f3(a, 0, y) -> y
f3(a, s1(x), y) -> f3(b, y, s1(x))
f3(b, y, x) -> f3(a, half1(x), exp1(y))
exp1(0) -> s1(0)
exp1(s1(x)) -> double1(exp1(x))
double1(0) -> 0
double1(s1(x)) -> s1(s1(double1(x)))
half1(0) -> double1(0)
half1(s1(0)) -> half1(0)
half1(s1(s1(x))) -> s1(half1(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
EXP1(s1(x)) -> EXP1(x)
tower1(x) -> f3(a, x, s1(0))
f3(a, 0, y) -> y
f3(a, s1(x), y) -> f3(b, y, s1(x))
f3(b, y, x) -> f3(a, half1(x), exp1(y))
exp1(0) -> s1(0)
exp1(s1(x)) -> double1(exp1(x))
double1(0) -> 0
double1(s1(x)) -> s1(s1(double1(x)))
half1(0) -> double1(0)
half1(s1(0)) -> half1(0)
half1(s1(s1(x))) -> s1(half1(x))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
EXP1(s1(x)) -> EXP1(x)
POL( EXP1(x1) ) = max{0, x1 - 2}
POL( s1(x1) ) = x1 + 3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
tower1(x) -> f3(a, x, s1(0))
f3(a, 0, y) -> y
f3(a, s1(x), y) -> f3(b, y, s1(x))
f3(b, y, x) -> f3(a, half1(x), exp1(y))
exp1(0) -> s1(0)
exp1(s1(x)) -> double1(exp1(x))
double1(0) -> 0
double1(s1(x)) -> s1(s1(double1(x)))
half1(0) -> double1(0)
half1(s1(0)) -> half1(0)
half1(s1(s1(x))) -> s1(half1(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
F3(b, y, x) -> F3(a, half1(x), exp1(y))
F3(a, s1(x), y) -> F3(b, y, s1(x))
tower1(x) -> f3(a, x, s1(0))
f3(a, 0, y) -> y
f3(a, s1(x), y) -> f3(b, y, s1(x))
f3(b, y, x) -> f3(a, half1(x), exp1(y))
exp1(0) -> s1(0)
exp1(s1(x)) -> double1(exp1(x))
double1(0) -> 0
double1(s1(x)) -> s1(s1(double1(x)))
half1(0) -> double1(0)
half1(s1(0)) -> half1(0)
half1(s1(s1(x))) -> s1(half1(x))